package com.googlecode.kipler.satisfiability.completion.branching;

import com.googlecode.kipler.container.dl.ABox;
import com.googlecode.kipler.container.dl.DependencySet;
import com.googlecode.kipler.container.dl.Individual;
import com.googlecode.kipler.container.dl.WorldConstraintSystem;
import com.googlecode.kipler.satisfiability.completion.rule.individual.MergePair;
import com.googlecode.kipler.satisfiability.completion.rule.individual.MergeStrategy;
import com.googlecode.kipler.satisfiability.reasoner.UnsatisfiableException;
import com.googlecode.kipler.syntax.formula.SameIndividualAssertion;

/**
 * 
 * @author İnanç Seylan
 * 
 */
public class IdentificationBranchingPoint extends BranchingPoint {
	private int index;

	private Individual individual;

	private WorldConstraintSystem newWcs;

	private MergeStrategy mergeStrategy;

	private MergePair mergePair;

	public MergePair getMergePair() {
		return mergePair;
	}

	public void setMergePair(MergePair mergePair) {
		this.mergePair = mergePair;
	}

	public Individual getIndividual() {
		return individual;
	}

	public void setIndividual(Individual individual) {
		this.individual = individual;
	}

	public MergeStrategy getMergeStrategy() {
		return mergeStrategy;
	}

	public void setMergeStrategy(MergeStrategy mergeStrategy) {
		this.mergeStrategy = mergeStrategy;
	}

	@Override
	public boolean isBranchingPossible() {
		return index < 2;
	}

	@Override
	public WorldConstraintSystem nextBranch() throws UnsatisfiableException {
		if (index == 0) {
			newWcs = getWcs().copy();
			newWcs.setId(getWcs().getId() + 1);
			index++;
			ABox newABox = newWcs.getWorld(getWorld().getName()).getABox();
			getMergeStrategy().merge(getIndividual().getName(), newABox,
					getMergePair(), createDependencySet());
			newWcs.getData().getLogger().info(
					"WCS " + newWcs.getId() + " At most rule: Merged "
							+ getMergePair().getFrom() + " into "
							+ getMergePair().getInto());
		} else if (index == 1) {
			newWcs = getWcs();
			SameIndividualAssertion ia = new SameIndividualAssertion(
					getMergePair().getFrom(), getMergePair().getInto())
					.toggleNegated();
			getLastBranchDependencies().remove(getWcs());
			newWcs.getData().getDependencyManager().addAll(ia,
					getLastBranchDependencies());
			newWcs.getWorld(getWorld().getName()).add(ia);
			index++;
		}
		return newWcs;
	}

	private DependencySet createDependencySet() {
		DependencySet result = new DependencySet();
		result.add(getWcs());
		return result;
	}

	@Override
	public void backtrack() {
		// TODO Auto-generated method stub

	}

}
